interface{-}check($D$;$l$;${\it tg}$;$T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$T$ $\subseteq\rho$ M(destination($l$)).din($l$,${\it tg}$)